COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 know4.lsp[f81,jmc]	comments and axioms on Kripke type knowledge
C00003 ENDMK
C⊗;
;;; know4.lsp[f81,jmc]	comments and axioms on Kripke type knowledge

;;; To say that  s  knows exactly  baz  and whether  p, we write

∀w1.a(w,w1,s) ⊃ baz(w1) = baz(w) ∧ (p(w1) ≡ p(w)) ∧
∀x.baz(w) = x ⊃ ∃w1.baz(w1)=x ∧ (p(w1) ≡ p(w))

;;; To say that  s  knows exactly  foo  and  baz, we
;;; define  mumph(w) = cons(foo(w),baz(w))